Bob is blue. Charlie is quiet. Gary is young. Harry is quiet. All blue, big people are smart. If someone is round then they are smart. All round people are young. If someone is quiet and not blue then they are round. All quiet, big people are round. Quiet people are big.
Bob is blue.
("Bob" "is" "blue" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
All blue, big people are smart.
((("someone" "is" "blue" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
If someone is round then they are smart.
((("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
All round people are young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
If someone is quiet and not blue then they are round.
((("someone" "is" "quiet" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "round" "+"))
All quiet, big people are round.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
Quiet people are big.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
Bob is blue.
True
1
proof
[(triple1)]
("Bob" "is" "blue" "+")
triple1
Harry is not quiet.
False
1
inv-proof
[(triple4)]
("Harry" "is" "quiet" "-")
triple4
Harry is big.
True
2
proof
[(((triple4) -> rule6))]
("Harry" "is" "big" "+")
((triple4) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Charlie is not big.
False
2
inv-proof
[(((triple2) -> rule6))]
("Charlie" "is" "big" "-")
((triple2) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Harry is round.
True
4
proof
[(((triple4 ((triple4) -> rule6)) -> rule5))]
("Harry" "is" "round" "+")
((triple4 ((triple4) -> (rule6 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Charlie is not round.
False
4
inv-proof
[(((triple2 ((triple2) -> rule6)) -> rule5))]
("Charlie" "is" "round" "-")
((triple2 ((triple2) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is young.
True
5
proof
[(((((triple2 ((triple2) -> rule6)) -> rule5)) -> rule3))]
("Charlie" "is" "young" "+")
((((triple2 ((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is not young.
False
5
inv-proof
[(((((triple2 ((triple2) -> rule6)) -> rule5)) -> rule3))]
("Charlie" "is" "young" "-")
((((triple2 ((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Bob is not young.
Unknown
inv-rconc
[@2: Bob is young.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Bob" "is" "young" "-")
Bob is big.
Unknown
rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "big" "+")
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "round" "-")
Bob is smart.
Unknown
rconc
[@2: Bob is smart.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("Bob" "is" "smart" "+")
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is blue.[(triple1)] Charlie is quiet.[(triple2)] Gary is young.[(triple3)] Harry is quiet.[(triple4)] @1: Charlie is big.[(((triple2) -> rule6))] Harry is big.[(((triple4) -> rule6))] @2: Charlie is round.[(((triple2 ((triple2) -> rule6)) -> rule5))] Harry is round.[(((triple4 ((triple4) -> rule6)) -> rule5))] @3: Charlie is smart.[(((((triple2 ((triple2) -> rule6)) -> rule5)) -> rule2))] Charlie is young.[(((((triple2 ((triple2) -> rule6)) -> rule5)) -> rule3))] Harry is smart.[(((((triple4 ((triple4) -> rule6)) -> rule5)) -> rule2))] Harry is young.[(((((triple4 ((triple4) -> rule6)) -> rule5)) -> rule3))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Gary is young.
("Gary" "is" "young" "+")
triple3
Harry is quiet.
("Harry" "is" "quiet" "+")
triple4
Charlie is big.
("Charlie" "is" "big" "+")
((triple2) -> (rule6 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple4) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple2 ((triple2) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((triple4 ((triple4) -> (rule6 % int2))) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple2 ((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
((((triple2 ((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
((((triple4 ((triple4) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
((((triple4 ((triple4) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3