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