Charlie is young. Dave is white. Fiona is young. If someone is white and big then they are blue. All white people are big. If someone is quiet then they are smart. Big people are smart. Cold people are big. All smart, white people are quiet.
Charlie is young.
("Charlie" "is" "young" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is young.
("Fiona" "is" "young" "+")
If someone is white and big then they are blue.
((("someone" "is" "white" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
All white people are big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
If someone is quiet then they are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
Big people are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
Cold people are big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
All smart, white people are quiet.
((("someone" "is" "smart" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
Dave is white.
True
1
proof
[(triple2)]
("Dave" "is" "white" "+")
triple2
Charlie is not young.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "young" "-")
triple1
Dave is big.
True
2
proof
[(((triple2) -> rule2))]
("Dave" "is" "big" "+")
((triple2) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not big.
False
2
inv-proof
[(((triple2) -> rule2))]
("Dave" "is" "big" "-")
((triple2) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is blue.
True
4
proof
[(((triple2 ((triple2) -> rule2)) -> rule1))]
("Dave" "is" "blue" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is not blue.
False
4
inv-proof
[(((triple2 ((triple2) -> rule2)) -> rule1))]
("Dave" "is" "blue" "-")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is quiet.
True
5
proof
[(((((((triple2) -> rule2)) -> rule4) triple2) -> rule6))]
("Dave" "is" "quiet" "+")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2)) triple2) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is not quiet.
False
5
inv-proof
[(((((((triple2) -> rule2)) -> rule4) triple2) -> rule6))]
("Dave" "is" "quiet" "-")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2)) triple2) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Charlie is not blue.
Unknown
inv-rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "blue" "-")
Fiona is quiet.
Unknown
rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "quiet" "+")
Fiona is not big.
Unknown
inv-rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "big" "-")
Fiona is blue.
Unknown
rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "blue" "+")
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
@0: Charlie is young.[(triple1)] Dave is white.[(triple2)] Fiona is young.[(triple3)] @1: Dave is big.[(((triple2) -> rule2))] @2: Dave is blue.[(((triple2 ((triple2) -> rule2)) -> rule1))] Dave is smart.[(((((triple2) -> rule2)) -> rule4))] @3: Dave is quiet.[(((((((triple2) -> rule2)) -> rule4) triple2) -> rule6))]
Charlie is young.
("Charlie" "is" "young" "+")
triple1
Dave is white.
("Dave" "is" "white" "+")
triple2
Fiona is young.
("Fiona" "is" "young" "+")
triple3
Dave is big.
("Dave" "is" "big" "+")
((triple2) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2)) triple2) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3