Bob is big. Bob is green. Bob is white. Dave is big. Dave is green. Dave is red. Dave is round. Dave is white. Dave is young. Fiona is round. Fiona is white. Harry is green. Harry is red. Harry is round. Harry is young. Round people are big. All round people are cold. Cold people are young. All big people are round. All red, white people are young. If someone is red then they are round.
Bob is big.
("Bob" "is" "big" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
Round people are big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
All round people are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
Cold people are young.
((("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
All big people are round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
All red, white people are young.
((("someone" "is" "red" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "young" "+"))
If someone is red then they are round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
Dave is big.
True
1
proof
[(triple4 OR ((triple7) -> rule1) OR ((((triple6) -> rule6)) -> rule1))]
("Dave" "is" "big" "+")
triple4
((triple7) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((((triple6) -> (rule6 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Bob is not big.
False
1
inv-proof
[(triple1)]
("Bob" "is" "big" "-")
triple1
Harry is big.
True
2
proof
[(((triple14) -> rule1) OR ((((triple13) -> rule6)) -> rule1))]
("Harry" "is" "big" "+")
((triple14) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((((triple13) -> (rule6 % int2))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Bob is not round.
False
2
inv-proof
[(((triple1) -> rule4))]
("Bob" "is" "round" "-")
((triple1) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Fiona is young.
True
3
proof
[(((((triple10) -> rule2)) -> rule3))]
("Fiona" "is" "young" "+")
((((triple10) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Fiona is not young.
False
3
inv-proof
[(((((triple10) -> rule2)) -> rule3))]
("Fiona" "is" "young" "-")
((((triple10) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Bob is young.
True
4
proof
[(((((((triple1) -> rule4)) -> rule2)) -> rule3))]
("Bob" "is" "young" "+")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is not young.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule2)) -> rule3))]
("Bob" "is" "young" "-")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Harry is not white.
Unknown
inv-random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Fiona is red.
Unknown
random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "+")
@0: Bob is big.[(triple1)] Bob is green.[(triple2)] Bob is white.[(triple3)] Dave is big.[(triple4 OR ((triple7) -> rule1) OR ((((triple6) -> rule6)) -> rule1))] Dave is green.[(triple5)] Dave is red.[(triple6)] Dave is round.[(triple7 OR ((triple4) -> rule4) OR ((triple6) -> rule6))] Dave is white.[(triple8)] Dave is young.[(triple9 OR ((triple6 triple8) -> rule5) OR ((((triple7) -> rule2)) -> rule3) OR ((((((triple4) -> rule4)) -> rule2)) -> rule3) OR ((((((triple6) -> rule6)) -> rule2)) -> rule3))] Fiona is round.[(triple10)] Fiona is white.[(triple11)] Harry is green.[(triple12)] Harry is red.[(triple13)] Harry is round.[(triple14 OR ((triple13) -> rule6))] Harry is young.[(triple15 OR ((((triple14) -> rule2)) -> rule3) OR ((((((triple13) -> rule6)) -> rule2)) -> rule3))] @1: Bob is round.[(((triple1) -> rule4))] Dave is cold.[(((triple7) -> rule2) OR ((((triple4) -> rule4)) -> rule2) OR ((((triple6) -> rule6)) -> rule2))] Fiona is big.[(((triple10) -> rule1))] Fiona is cold.[(((triple10) -> rule2))] Harry is big.[(((triple14) -> rule1) OR ((((triple13) -> rule6)) -> rule1))] Harry is cold.[(((triple14) -> rule2) OR ((((triple13) -> rule6)) -> rule2))] @2: Bob is cold.[(((((triple1) -> rule4)) -> rule2))] Fiona is young.[(((((triple10) -> rule2)) -> rule3))] @3: Bob is young.[(((((((triple1) -> rule4)) -> rule2)) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
Dave is big.
("Dave" "is" "big" "+")
triple4
((triple7) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((((triple6) -> (rule6 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
triple5
Dave is red.
("Dave" "is" "red" "+")
triple6
Dave is round.
("Dave" "is" "round" "+")
triple7
((triple4) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple6) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
triple8
Dave is young.
("Dave" "is" "young" "+")
triple9
((triple6 triple8) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
((((((triple4) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
((((((triple6) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
triple10
Fiona is white.
("Fiona" "is" "white" "+")
triple11
Harry is green.
("Harry" "is" "green" "+")
triple12
Harry is red.
("Harry" "is" "red" "+")
triple13
Harry is round.
("Harry" "is" "round" "+")
triple14
((triple13) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple15
((((triple14) -> (rule2 % int2))) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((((triple13) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
((triple1) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((triple7) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((triple4) -> (rule4 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((triple6) -> (rule6 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
((triple10) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple10) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple14) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((((triple13) -> (rule6 % int2))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((triple14) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((triple13) -> (rule6 % int2))) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
((((triple10) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3