Bob is white. Harry is big. Harry is green. White people are quiet. Green, quiet people are rough. All rough, quiet people are white. All big people are young. All young people are quiet. If someone is quiet then they are rough. Rough people are big. If someone is quiet and green then they are rough.
Bob is white.
("Bob" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is green.
("Harry" "is" "green" "+")
White people are quiet.
((("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
Green, quiet people are rough.
((("someone" "is" "green" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
All rough, quiet people are white.
((("someone" "is" "rough" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
All big people are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
All young people are quiet.
((("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
If someone is quiet then they are rough.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
Rough people are big.
((("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
If someone is quiet and green then they are rough.
((("someone" "is" "quiet" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
Harry is green.
True
1
proof
[(triple3)]
("Harry" "is" "green" "+")
triple3
Harry is not big.
False
1
inv-proof
[(triple2)]
("Harry" "is" "big" "-")
triple2
Bob is quiet.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "quiet" "+")
((triple1) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Harry is not young.
False
2
inv-proof
[(((triple2) -> rule4))]
("Harry" "is" "young" "-")
((triple2) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is quiet.
True
3
proof
[(((((triple2) -> rule4)) -> rule5))]
("Harry" "is" "quiet" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is not quiet.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule5))]
("Harry" "is" "quiet" "-")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Bob is big.
True
4
proof
[(((((((triple1) -> rule1)) -> rule6)) -> rule7))]
("Bob" "is" "big" "+")
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Harry is not rough.
False
4
inv-proof
[(((((((triple2) -> rule4)) -> rule5)) -> rule6) OR ((triple3 ((((triple2) -> rule4)) -> rule5)) -> rule2) OR ((((((triple2) -> rule4)) -> rule5) triple3) -> rule8))]
("Harry" "is" "rough" "-")
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
((triple3 ((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2)) triple3) -> (rule8 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Bob is white.[(triple1)] Harry is big.[(triple2)] Harry is green.[(triple3)] @1: Bob is quiet.[(((triple1) -> rule1))] Harry is young.[(((triple2) -> rule4))] @2: Bob is rough.[(((((triple1) -> rule1)) -> rule6))] Harry is quiet.[(((((triple2) -> rule4)) -> rule5))] @3: Bob is big.[(((((((triple1) -> rule1)) -> rule6)) -> rule7))] Harry is rough.[(((((((triple2) -> rule4)) -> rule5)) -> rule6) OR ((triple3 ((((triple2) -> rule4)) -> rule5)) -> rule2) OR ((((((triple2) -> rule4)) -> rule5) triple3) -> rule8))] @4: Bob is young.[(((((((((triple1) -> rule1)) -> rule6)) -> rule7)) -> rule4))] Harry is white.[(((((((((triple2) -> rule4)) -> rule5)) -> rule6) ((((triple2) -> rule4)) -> rule5)) -> rule3) OR ((((triple3 ((((triple2) -> rule4)) -> rule5)) -> rule2) ((((triple2) -> rule4)) -> rule5)) -> rule3) OR ((((((((triple2) -> rule4)) -> rule5) triple3) -> rule8) ((((triple2) -> rule4)) -> rule5)) -> rule3))]
Bob is white.
("Bob" "is" "white" "+")
triple1
Harry is big.
("Harry" "is" "big" "+")
triple2
Harry is green.
("Harry" "is" "green" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple1) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple2) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
((triple3 ((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2)) triple3) -> (rule8 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
((((((((triple1) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
int4
Harry is white.
("Harry" "is" "white" "+")
((((((((triple2) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule6 % int2)) ((((triple2) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
((((triple3 ((((triple2) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule2 % int2)) ((((triple2) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
((((((((triple2) -> (rule4 % int4))) -> (rule5 % int3)) triple3) -> (rule8 % int2)) ((((triple2) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4