Bob is blue. Charlie is quiet. All blue, smart things are nice. Rough things are nice. If something is round then it is rough. If something is smart then it is blue. Quiet, blue things are rough. All round things are blue. If something is nice then it is smart. Quiet things are round.
Bob is blue.
("Bob" "is" "blue" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
All blue, smart things are nice.
((("something" "is" "blue" "+") ("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
Rough things are nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
If something is round then it is rough.
((("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
If something is smart then it is blue.
((("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
Quiet, blue things are rough.
((("something" "is" "quiet" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
All round things are blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
If something is nice then it is smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
Quiet things are round.
((("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
Charlie is quiet.
True
1
proof
[(triple2)]
("Charlie" "is" "quiet" "+")
triple2
Bob is not blue.
False
1
inv-proof
[(triple1)]
("Bob" "is" "blue" "-")
triple1
Charlie is round.
True
2
proof
[(((triple2) -> rule8))]
("Charlie" "is" "round" "+")
((triple2) -> (rule8 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is not round.
False
2
inv-proof
[(((triple2) -> rule8))]
("Charlie" "is" "round" "-")
((triple2) -> (rule8 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is rough.
True
3
proof
[(((((triple2) -> rule8)) -> rule3) OR ((triple2 ((((triple2) -> rule8)) -> rule6)) -> rule5))]
("Charlie" "is" "rough" "+")
((((triple2) -> (rule8 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((triple2 ((((triple2) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is not rough.
False
3
inv-proof
[(((((triple2) -> rule8)) -> rule3) OR ((triple2 ((((triple2) -> rule8)) -> rule6)) -> rule5))]
("Charlie" "is" "rough" "-")
((((triple2) -> (rule8 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((triple2 ((((triple2) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is nice.
True
4
proof
[(((((((triple2) -> rule8)) -> rule3)) -> rule2) OR ((((triple2 ((((triple2) -> rule8)) -> rule6)) -> rule5)) -> rule2))]
("Charlie" "is" "nice" "+")
((((((triple2) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
((((triple2 ((((triple2) -> (rule8 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
Charlie is not nice.
False
4
inv-proof
[(((((((triple2) -> rule8)) -> rule3)) -> rule2) OR ((((triple2 ((((triple2) -> rule8)) -> rule6)) -> rule5)) -> rule2))]
("Charlie" "is" "nice" "-")
((((((triple2) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
((((triple2 ((((triple2) -> (rule8 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
Bob is not rough.
Unknown
inv-rconc
[@2: Bob is rough.[CWA. Example of deepest failure = (rule3 <- rule8 <- FAIL)]]
("Bob" "is" "rough" "-")
Bob is smart.
Unknown
rconc
[@4: Bob is smart.[CWA. Example of deepest failure = (rule7 <- rule2 <- rule3 <- rule8 <- FAIL)]]
("Bob" "is" "smart" "+")
Bob is not nice.
Unknown
inv-rconc
[@5: Bob is nice.[CWA. Example of deepest failure = (rule1 <- rule7 <- rule2 <- rule3 <- rule8 <- FAIL)]]
("Bob" "is" "nice" "-")
Bob is round.
Unknown
rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Bob" "is" "round" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Bob is blue.[(triple1)] Charlie is quiet.[(triple2)] @1: Charlie is round.[(((triple2) -> rule8))] @2: Charlie is blue.[(((((triple2) -> rule8)) -> rule6) OR ((((((((((triple2) -> rule8)) -> rule3)) -> rule2)) -> rule7)) -> rule4))] Charlie is rough.[(((((triple2) -> rule8)) -> rule3) OR ((triple2 ((((triple2) -> rule8)) -> rule6)) -> rule5))] @3: Charlie is nice.[(((((((triple2) -> rule8)) -> rule3)) -> rule2) OR ((((triple2 ((((triple2) -> rule8)) -> rule6)) -> rule5)) -> rule2))] @4: Charlie is smart.[(((((((((triple2) -> rule8)) -> rule3)) -> rule2)) -> rule7) OR ((((((triple2 ((((triple2) -> rule8)) -> rule6)) -> rule5)) -> rule2)) -> rule7))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Charlie is round.
("Charlie" "is" "round" "+")
((triple2) -> (rule8 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple2) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((((((((((triple2) -> (rule8 % int5))) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
int4
Charlie is round.
("Charlie" "is" "round" "+")
int5
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple2) -> (rule8 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((triple2 ((((triple2) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
((((((triple2) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
((((triple2 ((((triple2) -> (rule8 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
Charlie is smart.
("Charlie" "is" "smart" "+")
((((((((triple2) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
((((((triple2 ((((triple2) -> (rule8 % int5))) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
Charlie is round.
("Charlie" "is" "round" "+")
int5