Bob is young. Dave is big. Harry is big. All big, young people are blue. If Dave is rough then Dave is blue. If someone is big then they are young. Red people are big. If someone is young then they are red. All young, blue people are rough. Red, round people are young. If someone is young then they are blue.
Bob is young.
("Bob" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Harry is big.
("Harry" "is" "big" "+")
All big, young people are blue.
((("someone" "is" "big" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
If Dave is rough then Dave is blue.
((("Dave" "is" "rough" "+")) -> ("Dave" "is" "blue" "+"))
If someone is big then they are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
Red people are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If someone is young then they are red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
All young, blue people are rough.
((("someone" "is" "young" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
Red, round people are young.
((("someone" "is" "red" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
If someone is young then they are blue.
((("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
Dave is big.
True
1
proof
[(triple2)]
("Dave" "is" "big" "+")
triple2
Bob is not young.
False
1
inv-proof
[(triple1)]
("Bob" "is" "young" "-")
triple1
Bob is blue.
True
2
proof
[(((triple1) -> rule8) OR ((((((triple1) -> rule5)) -> rule4) triple1) -> rule1))]
("Bob" "is" "blue" "+")
((triple1) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2)) triple1) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is not red.
False
2
inv-proof
[(((triple1) -> rule5))]
("Bob" "is" "red" "-")
((triple1) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
@0: Bob is young.[(triple1)] Dave is big.[(triple2)] Harry is big.[(triple3)] @1: Bob is blue.[(((triple1) -> rule8) OR ((((((triple1) -> rule5)) -> rule4) triple1) -> rule1))] Bob is red.[(((triple1) -> rule5))] Dave is young.[(((triple2) -> rule3))] Harry is young.[(((triple3) -> rule3))] @2: Bob is big.[(((((triple1) -> rule5)) -> rule4))] Bob is rough.[(((triple1 ((triple1) -> rule8)) -> rule6) OR ((triple1 ((((((triple1) -> rule5)) -> rule4) triple1) -> rule1)) -> rule6))] Dave is blue.[(((((triple2) -> rule3)) -> rule8) OR ((triple2 ((triple2) -> rule3)) -> rule1))] Dave is red.[(((((triple2) -> rule3)) -> rule5))] Harry is blue.[(((((triple3) -> rule3)) -> rule8) OR ((triple3 ((triple3) -> rule3)) -> rule1))] Harry is red.[(((((triple3) -> rule3)) -> rule5))] @3: Dave is rough.[(((((triple2) -> rule3) ((((triple2) -> rule3)) -> rule8)) -> rule6) OR ((((triple2) -> rule3) ((triple2 ((triple2) -> rule3)) -> rule1)) -> rule6))] Harry is rough.[(((((triple3) -> rule3) ((((triple3) -> rule3)) -> rule8)) -> rule6) OR ((((triple3) -> rule3) ((triple3 ((triple3) -> rule3)) -> rule1)) -> rule6))]
Bob is young.
("Bob" "is" "young" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Harry is big.
("Harry" "is" "big" "+")
triple3
Bob is blue.
("Bob" "is" "blue" "+")
((triple1) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2)) triple1) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
((triple1) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple2) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple3) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((triple1 ((triple1) -> (rule8 % int2))) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((triple1 ((((((triple1) -> (rule5 % int4))) -> (rule4 % int3)) triple1) -> (rule1 % int2))) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
Dave is blue.
("Dave" "is" "blue" "+")
((((triple2) -> (rule3 % int2))) -> (rule8 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
((triple2 ((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
((((triple3) -> (rule3 % int2))) -> (rule8 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((triple3 ((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((((triple2) -> (rule3 % int3)) ((((triple2) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
((((triple2) -> (rule3 % int3)) ((triple2 ((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
((((triple3) -> (rule3 % int3)) ((((triple3) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
((((triple3) -> (rule3 % int3)) ((triple3 ((triple3) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3