Bob is big. Bob is blue. Bob is cold. Bob is rough. Fiona is big. Fiona is cold. Fiona is kind. Fiona is round. Harry is big. Harry is cold. Harry is nice. Harry is round. If something is blue then it is round. If something is big and nice then it is blue. All blue things are cold. All big things are blue. All rough, big things are kind. If something is kind and blue then it is round.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is round.
("Harry" "is" "round" "+")
If something is blue then it is round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
If something is big and nice then it is blue.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
All blue things are cold.
((("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
All big things are blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
All rough, big things are kind.
((("something" "is" "rough" "+") ("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
If something is kind and blue then it is round.
((("something" "is" "kind" "+") ("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
Harry is nice.
True
1
proof
[(triple11)]
("Harry" "is" "nice" "+")
triple11
Bob is not cold.
False
1
inv-proof
[(triple3 OR ((triple2) -> rule3) OR ((((triple1) -> rule4)) -> rule3))]
("Bob" "is" "cold" "-")
triple3
((triple2) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Harry is not kind.
Unknown
inv-rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "kind" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
@0: Bob is big.[(triple1)] Bob is blue.[(triple2 OR ((triple1) -> rule4))] Bob is cold.[(triple3 OR ((triple2) -> rule3) OR ((((triple1) -> rule4)) -> rule3))] Bob is rough.[(triple4)] Fiona is big.[(triple5)] Fiona is cold.[(triple6 OR ((((triple5) -> rule4)) -> rule3))] Fiona is kind.[(triple7)] Fiona is round.[(triple8 OR ((((triple5) -> rule4)) -> rule1) OR ((triple7 ((triple5) -> rule4)) -> rule6))] Harry is big.[(triple9)] Harry is cold.[(triple10 OR ((((triple9) -> rule4)) -> rule3) OR ((((triple9 triple11) -> rule2)) -> rule3))] Harry is nice.[(triple11)] Harry is round.[(triple12 OR ((((triple9) -> rule4)) -> rule1) OR ((((triple9 triple11) -> rule2)) -> rule1))] @1: Bob is kind.[(((triple4 triple1) -> rule5))] Bob is round.[(((triple2) -> rule1) OR ((((triple1) -> rule4)) -> rule1) OR ((((triple4 triple1) -> rule5) triple2) -> rule6) OR ((((triple4 triple1) -> rule5) ((triple1) -> rule4)) -> rule6))] Fiona is blue.[(((triple5) -> rule4))] Harry is blue.[(((triple9) -> rule4) OR ((triple9 triple11) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
((triple1) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
triple3
((triple2) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
triple4
Fiona is big.
("Fiona" "is" "big" "+")
triple5
Fiona is cold.
("Fiona" "is" "cold" "+")
triple6
((((triple5) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
triple7
Fiona is round.
("Fiona" "is" "round" "+")
triple8
((((triple5) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
((triple7 ((triple5) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
triple9
Harry is cold.
("Harry" "is" "cold" "+")
triple10
((((triple9) -> (rule4 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple9 triple11) -> (rule2 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
triple11
Harry is round.
("Harry" "is" "round" "+")
triple12
((((triple9) -> (rule4 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple9 triple11) -> (rule2 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
((triple4 triple1) -> (rule5 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple2) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((triple4 triple1) -> (rule5 % int2)) triple2) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple4 triple1) -> (rule5 % int3)) ((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple5) -> (rule4 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple9) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple9 triple11) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1