Anne is round. Bob is kind. Charlie is big. Charlie is quiet. Charlie is rough. Charlie is young. Harry is young. If someone is round then they are big. If Anne is quiet then Anne is not round. Round people are young. If someone is rough and quiet then they are round. If Charlie is big and Charlie is not round then Charlie is red. All round people are not red. If someone is kind and not rough then they are red. If Bob is rough and Bob is not big then Bob is kind.
Anne is round.
("Anne" "is" "round" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is round then they are big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
If Anne is quiet then Anne is not round.
((("Anne" "is" "quiet" "+")) -> ("Anne" "is" "round" "-"))
Round people are young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
If someone is rough and quiet then they are round.
((("someone" "is" "rough" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
If Charlie is big and Charlie is not round then Charlie is red.
((("Charlie" "is" "big" "+") ("Charlie" "is" "round" "~")) -> ("Charlie" "is" "red" "+"))
All round people are not red.
((("someone" "is" "round" "+")) -> ("someone" "is" "red" "-"))
If someone is kind and not rough then they are red.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "red" "+"))
If Bob is rough and Bob is not big then Bob is kind.
((("Bob" "is" "rough" "+") ("Bob" "is" "big" "~")) -> ("Bob" "is" "kind" "+"))
Charlie is young.
True
1
proof
[(triple6 OR ((((triple5 triple4) -> rule4)) -> rule3))]
("Charlie" "is" "young" "+")
triple6
((((triple5 triple4) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is not big.
False
1
inv-proof
[(triple3 OR ((((triple5 triple4) -> rule4)) -> rule1))]
("Charlie" "is" "big" "-")
triple3
((((triple5 triple4) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is round.
True
3
proof
[(((triple5 triple4) -> rule4))]
("Charlie" "is" "round" "+")
((triple5 triple4) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is not round.
False
3
inv-proof
[(((triple5 triple4) -> rule4))]
("Charlie" "is" "round" "-")
((triple5 triple4) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is not red.
True
4
proof
[(((((triple5 triple4) -> rule4)) -> rule6))]
("Charlie" "is" "red" "-")
((((triple5 triple4) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is red.
False
4
inv-proof
[(((((triple5 triple4) -> rule4)) -> rule6))]
("Charlie" "is" "red" "+")
((((triple5 triple4) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Harry" "is" "red" "-")
Bob is big.
Unknown
rconc
[@2: Bob is big.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Bob" "is" "big" "+")
Harry is not round.
Unknown
inv-rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "round" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Anne is round.[(triple1)] Bob is kind.[(triple2)] Charlie is big.[(triple3 OR ((((triple5 triple4) -> rule4)) -> rule1))] Charlie is quiet.[(triple4)] Charlie is rough.[(triple5)] Charlie is young.[(triple6 OR ((((triple5 triple4) -> rule4)) -> rule3))] Harry is young.[(triple7)] @1: Anne is big.[(((triple1) -> rule1))] Anne is not red.[(((triple1) -> rule6))] Anne is young.[(((triple1) -> rule3))] Charlie is round.[(((triple5 triple4) -> rule4))] @2: Charlie is not red.[(((((triple5 triple4) -> rule4)) -> rule6))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Charlie is big.
("Charlie" "is" "big" "+")
triple3
((((triple5 triple4) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
Charlie is young.
("Charlie" "is" "young" "+")
triple6
((((triple5 triple4) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
triple7
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not red.
("Anne" "is" "red" "-")
((triple1) -> (rule6 % int1))
Anne is not red.
("Anne" "is" "red" "-")
int1
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple5 triple4) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is not red.
("Charlie" "is" "red" "-")
((((triple5 triple4) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2