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